#include <stdio.h>
#include <stdlib.h>
#include <time.h>
#include <string.h>
#include "matrice.h"
#include "fsio.h"
#include "solver.h"
#include "mem.h"

clock_t start_time;
int nb_threads_dispo;

int mode_benchmark = 0;
int mode_afficher_clauses = 0;
int mode_afficher_solution = 0;

extern t_litteral* solution;

int main (int argc, char *argv[])
{

	int res, i;
	t_clause* tab_clauses;
	t_litteral* tab_variables;

	t_matrice matrice;
	
	if (argc < 3)
	{
		printf("Utilisation : %s donnees.txt nombre_de_threads [bcs]\n\n", argv[0]);
		return -1;
	}
	
	nb_threads_dispo = atoi(argv[2]);
	
	if (argc >= 4)
	{
		for (i=0; argv[3][i] != '\0'; i++)
		{
			switch (argv[3][i])
			{
				case 'b': mode_benchmark = 1; break;
				case 'c': mode_afficher_clauses = 1; break;
				case 's': mode_afficher_solution = 1; break;
			}
		}
	}
	
	if (!mode_benchmark)
	{	
		printf("                   __             __               \n");
		printf("  ______________ _/ /__________  / /   _____  _____\n");
		printf(" / ___/ ___/ __ `/ __/ ___/ __ \\/ / | / / _ \\/ ___/\n");
		printf("/ /__(__  ) /_/ / /_(__  ) /_/ / /| |/ /  __/ /    \n");
		printf("\\___/____/\\__,_/\\__/____/\\____/_/ |___/\\___/_/ \n\n");

		printf("Threads : %d\n", nb_threads_dispo);
	}
	
	/* Charger le fichier */
	if (charger(&matrice, &tab_clauses, &tab_variables, argv[1]) < 0)
	{
		printf("Le fichier %s n'existe pas ou n'est pas accessible.\n\n", argv[1]);
		return -2;
	}

	if (!mode_benchmark) {
		printf("Chargement terminé !\n");
	}
	
	srand(time(NULL));
	
	/* Demarrer le timer */
	start_time = clock();
	
	/* Initialiser le multithreading */
	if (nb_threads_dispo)
	{
		init_threading();
		init_mem_threading();
	}
	
	/* Lancer le calcul :-) */
	res = resoudre(&matrice, tab_clauses, tab_variables, 0);

	if (!mode_benchmark)
	{
		if (res == 1)
		{
			printf("La formule est satisfiable.\n\n");
			if (mode_afficher_solution)
			{
				afficher_tab_variables (solution, nombre_variables(solution));
			}
		} else {
			printf("Aucune solution !\n");
		}
	
		printf("\nTemps de calcul : %f\n", (clock() - start_time)/1000000.F);
		printf("Nombre d'allocations internes : %d\nNombre d'allocations système (malloc) : %d\n", nombre_alloc(), nombre_malloc());
	} else {
		/* Mode benchmark -> affichage CSV (Comma Separated Values) */
		/* NOM_DU_FICHIER,NOMBRE_DE_VARIABLES,NOMBRE_DE_CLAUSES,RESULTAT,TEMPS */
		printf("%s,%d,%d,", argv[1], nombre_variables(tab_variables), nombre_clauses(tab_clauses));
		if (res == 1)
		{
			printf("1");
		} else {
			printf("0");
		}
		printf(",%f\n", (clock() - start_time)/1000000.F);
	}

	/* Code erreur 1 s'il existe un modèle, -1 sinon */
	return res;
}
